COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "memo.pub[let,jmc]" source
C00005 ENDMK
C⊗;
.require "memo.pub[let,jmc]" source;
.cb Correctness of Programs that Modify List Structure

	Consider the LISP program ⊗nconc defined by

nconc[u,v] ← qif qn u qthen v
		qelse prog[[w]
	w ← u
l:	qif qn qd w qthen qbegin jnk ← rplacd[w,v]; return u qend;
	w ← qd w
	qgo l]


	⊗nconc is a destructive version of ⊗append in that a variable
whose value is ⊗u is changed to have value ⊗u*v.
Other variables are unchanged if they don't merge with the top
level of ⊗u.  How shall we state this formally and prove it?

	We begin by distinguishing between S-expressions and
pointers and by introducing the memory state ⊗mem and
the function ⊗val(uu,m).  We shall use single letters for variables
whose values are S-expressions and doubled letters for variables whose
values are pointers.  A typical relation might be

	%2val(xx,mem) = x%1

meaning that the pointer ⊗xx points to a list structure representing
the S-expression which is the value of the S-expression variable
⊗x.  

	We now introduce ⊗nconc(xx,_vv,_mem) as a two output function
whose value is a new pointer and a new memory state.  We shall
want to prove

	%2∀uu mem. val(nconc(uu, vv, mem) = val(uu, mem) * val(vv, mem)%1

as the relation between ⊗nconc and ⊗append. 
However, this isn't all we will need to prove about ⊗nconc. 

	The program can now be written cleanly as

%2nconc[uu, vv, mem] ← qif null[uu, mem] qthen vv, mem
			qelse prog[[ww, jjnk]
	ww ← uu;
l:	qif null cdr[ww, mem] qthen 
		qbegin jjnk, mem ← rplacd[ww, vv, mem] return2[uu, mem] qend;
	ww ← cdr[ww, mem];
	qgo l]%1.

	Perhaps we should now try to elephantize the program, but it
still isn't clear how to elephantize function calls.